//
//  wrapper.cpp
//  ltlbmc
//
//  Created by GD Huang on 7/10/12.
//  Copyright (c) 2012 __MyCompanyName__. All rights reserved.
//

#include <iostream>




#include <stdlib.h>
#include <stdarg.h>
#include <stdio.h>
#include <assert.h>
#include "wrapper.h"

#ifdef DEBUG
#define dprint(x,...) printf(x,__VA_ARGS__)
#else
#define dprint(x,...) 
#endif

int GetVarInt(Manager mng, int size, int* vars) {
	int i, j, res;
	for(i=0, res=0; i<size; i++) {
        j = GetVar(mng, vars[i]);
        if(j==-1) {//-1 means UNKNOWN or undicided
            dprint("%d is undicided", vars[i]);
            j=0;
        }  
		res = res + (j<<i);
	}
	return res;
}


void dump_vars(Manager mng) {
	int i;
	for(i=FF; i<NumVars(mng); i++) { //FF is the first var
        if(i%10==0)
            printf("%d\t", i);
		printf("%d ", GetVar(mng,i));
        if(i%10==9)
            printf("\n");
	}
    printf("\n");
}

inline void addCls1(Manager mng, int a) {
	int cls[1] = { a };
	AddClause(mng, 1, cls) ;
}

inline void addCls2(Manager mng, int a, int b) {
	int cls[2] = { a,b };
	AddClause(mng, 2, cls) ;
}

inline void addCls3(Manager mng, int a, int b, int c) {
	int cls[3] = { a, b, c };
	AddClause(mng, 3, cls) ;
}

inline void addCls4(Manager mng, int a, int b, int c, int d) {
	int cls[4] = { a, b, c, d };
	AddClause(mng, 4, cls) ;
}

inline void addCls5(Manager mng, int a, int b, int c, int d, int e) {
	int cls[5] = { a, b, c, d, e };
	AddClause(mng, 5, cls) ;
}

int* NewVarS(Manager mng, int size, int dvar) {
	int* res;
	int i;
    
	res = (int*)malloc(sizeof(int)*size);
	for(i=0; i<size; i++)
  		res[i] = NewVar(mng, dvar);
	return res;
}

/*
 size: the total size of gate inputs
 predef_size: the size of given inputs
 */
int* NewVarGate(Manager mng, int size, int dvar, GATE gate, int predef_size, int o, ...) {
	va_list argptr;
	int* res;
	int i;
	
	assert(predef_size<=size);
	res = (int*)malloc(sizeof(int)*size);
	va_start(argptr, o);
	for(i=0; i<predef_size; i++) {
		res[i] = va_arg (argptr,int);
	}
	va_end(argptr);
	for(;i<size; i++) {
		res[i] = NewVar(mng, dvar);
	}
    
	(*gate)(mng, size, o, res);
	return res;  	
}

/*
 lsb ... msb
 alist = a0 a1 ...
 blist = b0 b1 ...
 */
int* int2bools(Manager mng, int size, int c) {
	assert(mng);
	int* bools = (int*)malloc(size*sizeof(int));
	int i;
    
	for(i=0; i<size; i++) {
		bools[i] = c&1 ? TT:FF;
		c = c>>1;
	}
    
	if(c>0)  printf("sat_wrapper.c:int2bools(): constant overflow\n"), exit(1);
    
	return bools;	
}




void Assert(Manager mng, int o) {
    dprint("Assert %d\n", o);
	addCls1(mng, pos(o));
}

void AssertNot(Manager mng, int o) {
    dprint("AssertNot %d\n", o);
	addCls1(mng, neg(o));
}

void Imply(Manager mng, int a, int b) {
    dprint("Imply %d %d\n", a, b);
	addCls2(mng, neg(a), pos(b));	
}

void ImplyNot(Manager mng, int a, int b) {
    dprint("ImplyNot %d %d\n", a, b);
	addCls2(mng, neg(a), neg(b));	
}

void Or2(Manager mng, int o, int a, int b) {
    dprint("Or %d %d %d\n", o, a, b);
	addCls3(mng, neg(o), pos(a), pos(b));
    
	addCls2(mng, pos(o), neg(a));
	addCls2(mng, pos(o), neg(b));
}

void Or3(Manager mng, int o, int a, int b, int c) {
    dprint("Or3 %d %d %d %d\n", o, a, b, c);
	addCls4(mng, neg(o), pos(a), pos(b), pos(c));
    
	addCls2(mng, pos(o), neg(a));
	addCls2(mng, pos(o), neg(b));	
	addCls2(mng, pos(o), neg(c));
}

void Or(Manager mng, int size, int o, int* a) {
	int cls[1+size];
	int i;
    
	assert(size>0);
    dprint("Or %d", o);	
	for(i=0; i<size; i++) {
        dprint(" %d", a[i]);
		cls[i] = pos(a[i]);
		addCls2(mng, pos(o), neg(a[i]));
	}
    dprint("%s","\n");
	cls[i] = neg(o);
	AddClause(mng, 1+size, cls);
}


void And2(Manager mng, int o, int a, int b) {
    dprint("And2 %d %d %d\n", o, a, b);
	addCls2(mng, neg(o), pos(a));
	addCls2(mng, neg(o), pos(b));	
    
	addCls3(mng, pos(o), neg(a), neg(b));
}

void And3(Manager mng, int o, int a, int b, int c) {
    dprint("And3 %d %d %d %d\n", o, a, b, c);
	addCls2(mng, neg(o), pos(a));
	addCls2(mng, neg(o), pos(b));	
	addCls2(mng, neg(o), pos(c));
    
	addCls4(mng, pos(o), neg(a), neg(b), neg(c));
}

void And(Manager mng, int size, int o, int* a) {
	int cls[1+size];
	int i;
	
	assert(size>0);
    dprint("And %d ", o);
	for(i=0; i<size; i++) {
        dprint(" %d", a[i]);
		addCls2(mng, neg(o), pos(a[i]));
		cls[i] = neg(a[i]);
	}
    dprint("%s","\n");
	cls[i] = pos(o);
	AddClause(mng, 1+size, cls);
}


/* 
 o = a xor b
 (a' + b' + o')
 (a  + b  + o')
 (a' + b  + o )
 (a  + b' + o )
 */
void Xor(Manager mng, int o, int a, int b) {
    //dprint("Xor %d %d %d", o, a, b);
	addCls3(mng, neg(o), neg(a), neg(b));
	addCls3(mng, neg(o), pos(a), pos(b));
    
	addCls3(mng, pos(o), neg(a), pos(b));
	addCls3(mng, pos(o), pos(a), neg(b));
}

/* 
 o = a xnor b
 (a' + b  + o')
 (a  + b' + o')
 (a  + b  + o )
 (a' + b' + o )
 */
void XNor(Manager mng, int o, int a, int b) {
    //dprint("XNor %d %d %d", o, a, b);
	addCls3(mng, neg(o), neg(a), pos(b));
	addCls3(mng, neg(o), pos(a), neg(b));
    
	addCls3(mng, pos(o), pos(a), pos(b));
	addCls3(mng, pos(o), neg(a), neg(b));
}

/* 
 alist = a0 a1 ...
 blist = b0 b1 ...
 a0 xnor b0 /\ a1 xnor b1 /\ ...
 */
void Eq(Manager mng, int size, int o, int* a, int* b) {
	int* os;
	int i;
    
    dprint("Eq %d ", o);
	os = NewVarS(mng, size, 0);
	And(mng, size, o, os);
	for(i=0; i<size; i++) {
        dprint("(%d,%d) ", a[i], b[i]);
		XNor(mng, os[i], a[i], b[i]);	
	}
    dprint("%s","\n");
	free(os);
}


void Eq_const(Manager mng, int size, int o, int* a, int c) {
	int cls[1+size];
	int i;
	
	assert(size>0);
    dprint("Eq_const %d %d", o, c);
	for(i=0; i<size; i++) {		
        dprint(" %d", a[i]);
		if(c&1) {
			addCls2(mng, neg(o), pos(a[i]));
			cls[i] = neg(a[i]);
		} else {
			addCls2(mng, neg(o), neg(a[i]));
			cls[i] = pos(a[i]);
		}
		c = c>>1;
	}
    dprint("%s","\n");
	cls[size] = pos(o);
	AddClause(mng, 1+size, cls);
    
	if(c>0)  printf("sat_wrapper.c:Eq_const(): constant overflow\n"), exit(1);
}

/* 
 alist = a0 a1 ...
 blist = b0 b1 ...
 a0 xor b0 \/ a1 xor b1 \/ ...
 */
void Neq(Manager mng, int size, int o, int* a, int* b) {
	int* os;
	int i;
    
    dprint("Neq %d ", o);
	os = NewVarS(mng, size, 0);
	Or(mng, size, o, os);
	for(i=0; i<size; i++) {
        dprint("(%d,%d) ", a[i], b[i]);
		Xor(mng, os[i], a[i], b[i]); 
    }
    dprint("%s","\n");
	free(os);	
}

void Neq_const(Manager mng, int size, int o, int* a, int c) {
	int cls[1+size];
	int i;
    
    dprint("Neq_const %d %d", o, c);
	assert(size>0);	
	for(i=0; i<size; i++) {
        dprint(" %d", a[i]);				
		if(c&1) {
			addCls2(mng, pos(o), pos(a[i]));
			cls[i] = neg(a[i]);
		} else {
			addCls2(mng, pos(o), neg(a[i]));
			cls[i] = pos(a[i]);
		}
		c = c>>1;
	}
    dprint("%s","\n");
	cls[i] = neg(o);
	AddClause(mng, 1+size, cls);
    
	if(c>0)  printf("sat_wrapper.c:Neq_const(): constant overflow\n"), exit(1);
}

/*
 lsb ... msb
 alist = a0 a1 ...
 blist = b0 b1 ...
 */
void Lt(Manager mng, int size, int o, int* a, int* b) {
	int i; 
	int c;
	int lsb = o; //less significant bit
    
    dprint("Lt %d ", o);
	for(i=size-1; i>0; i--) {
        dprint("(%d,%d) ", a[i], b[i]);
		c = lsb;
		lsb = NewVar(mng, 0);
		// c -> (!a/\b) \/ (a/\b/\lsb) \/ (!a/\!b/\lsb)
		addCls3(mng, neg(c), neg(a[i]), pos(b[i]));
		addCls3(mng, neg(c), neg(a[i]), pos(lsb));
		addCls3(mng, neg(c), pos(b[i]), pos(lsb));
		// c <- (!a/\b) \/ (a/\b/\lsb) \/ (!a/\!b/\lsb)
		addCls3(mng, pos(c), pos(a[i]), neg(b[i]));    
		addCls4(mng, pos(c), neg(a[i]), neg(b[i]), neg(lsb));   
		addCls4(mng, pos(c), pos(a[i]), pos(b[i]), neg(lsb));   
	}
    dprint("%s","\n");
	// lsb -> (!a/\b)
	addCls2(mng, neg(lsb), neg(a[0]));
	addCls2(mng, neg(lsb), pos(b[0]));
	// lsb <- (!a/\b)
	addCls3(mng, pos(lsb), pos(a[0]), neg(b[0]));  	  	
}

void Leq(Manager mng, int size, int o, int* a, int* b) {
	int i; 
	int c;
	int lsb = o; //less significant bit
    
    dprint("Leq %d ", o);    
	for(i=size-1; i>0; i--) {
        dprint("(%d,%d) ", a[i], b[i]);
		c = lsb;
		lsb = NewVar(mng, 0);
		// c -> (!a/\b) \/ (a/\b/\lsb) \/ (!a/\!b/\lsb)
		addCls3(mng, neg(c), neg(a[i]), pos(b[i]));
		addCls3(mng, neg(c), neg(a[i]), pos(lsb));
		addCls3(mng, neg(c), pos(b[i]), pos(lsb));
		// c <- (!a/\b) \/ (a/\b/\lsb) \/ (!a/\!b/\lsb)
		addCls3(mng, pos(c), pos(a[i]), neg(b[i]));    
		addCls4(mng, pos(c), neg(a[i]), neg(b[i]), neg(lsb));   
		addCls4(mng, pos(c), pos(a[i]), pos(b[i]), neg(lsb));   
	}
    dprint("%s","\n");
	// lsb -> (!a\/b)
	addCls3(mng, neg(lsb), neg(a[0]), pos(b[0]));
	// lsb <- (!a\/b)
	addCls2(mng, pos(lsb), pos(a[0]));
	addCls2(mng, pos(lsb), neg(b[0]));
    
}

/*
 lsb ... msb
 alist = a0 a1 ...
 blist = b0 b1 ...
 
 o -> (res=a+b)
 */
void Sum_const(Manager mng, int size, int o, int* res, int* a, int b) {
    int i;
    int c;
    int carry = FF;
    
    dprint("Sum_const %d %d ", o, b);
    for(i=0; i<size; i++) {
        dprint("%d ", a[i]);
        c = carry;
        carry = NewVar(mng, 0);
        
        if(b&1) { //b=1
            //carry <-> c \/ a[i]
            addCls4(mng, neg(o), neg(carry), pos(c), pos(a[i]));
            addCls3(mng, neg(o), pos(carry), neg(c));
            addCls3(mng, neg(o), pos(carry), neg(a[i]));
            //o[i] <-> (c /\ a) \/ (!c /\ !a)
            addCls4(mng, neg(o), neg(res[i]), neg(c), pos(a[i]));
            addCls4(mng, neg(o), neg(res[i]), pos(c), neg(a[i]));
            addCls4(mng, neg(o), pos(res[i]), neg(c), neg(a[i]));
            addCls4(mng, neg(o), pos(res[i]), pos(c), pos(a[i]));
        } else {//b=0
            //carry <-> c /\ a[i]
            addCls3(mng, neg(o), neg(carry), pos(c));
            addCls3(mng, neg(o), neg(carry), pos(a[i]));
            addCls4(mng, neg(o), pos(carry), neg(c), neg(a[i]));
            // o[i] <-> (c /\ !a) \/ (!c /\ a)
            addCls4(mng, neg(o), neg(res[i]), pos(c), pos(a[i]));
            addCls4(mng, neg(o), neg(res[i]), neg(c), neg(a[i]));
            addCls4(mng, neg(o), pos(res[i]), neg(c), pos(a[i]));
            addCls4(mng, neg(o), pos(res[i]), pos(c), neg(a[i]));
        }
        b=b>>1;
    }
    dprint("%s","\n");
    //no overflow la
    addCls2(mng, neg(o), neg(carry));
    
    if(b>0)  printf("sat_wrapper.c:Sum_const(): constant overflow\n"), exit(1);
    
}


//o = a /\ (b\/c) 
void a_And_b_Or_c(Manager mng, int o, int a, int b, int c) {
    dprint("%d = %d /\\(%d \\/ %d)\n", o, a, b, c);
    addCls2(mng, neg(o), pos(a));
    addCls3(mng, neg(o), pos(b), pos(c));
    addCls3(mng, pos(o), neg(a), neg(b));
    addCls3(mng, pos(o), neg(a), neg(c));
}



